Nuprl Lemma : s-dsys_wf
0,22
postcript
pdf
M
:(Id
MsgA). s-dsys(
M
)
Dsys
latex
Definitions
Dsys
,
s-dsys(
M
)
,
x
:
A
.
B
(
x
)
,
Id
,
t
T
,
MsgA
Lemmas
msga
wf
,
Id
wf
origin
M:(Id
MsgA). s-dsys(M) 
Dsys M:(IdMsgA). s-dsys(M) Dsys x:A. B(x) T